Nuprl Lemma : atom-free-atom
0,22
postcript
pdf
a
:Atom. AtomFree(Atom;
a
)
latex
Definitions
Atom
,
t
T
,
AtomFree(
T
;
x
)
,
x
:
A
.
B
(
x
)
origin
a:Atom. AtomFree(Atom;a) a:Atom. AtomFree(Atom;a) 
Tx:A. B(x)